Nuprl Lemma : d-m_wf
0,22
postcript
pdf
D
:Dsys,
i
:Id. M(
i
)
MsgA
latex
Definitions
Dsys
,
M(
i
)
,
x
:
A
.
B
(
x
)
,
Id
,
t
T
,
MsgA
Lemmas
msga
wf
,
Id
wf
origin
D:Dsys, i:Id. M(i) 
MsgA D:Dsys, i:Id. M(i) MsgA x:A. B(x) T